Homotopy Type Theory, V
Posted by Mike Shulman
I think posts I-IV have more or less covered the current state of the art in homotopy type theory. I omitted a few things, like the fact that univalence implies function extensionality (but see below). I also didn’t talk too much about what people have proven inside homotopy type theory so far, like the fact that Ω² is abelian. But overall I think I gave a relatively complete picture (although knowledgable readers should feel free to object!).
What’s next is necessarily more speculative. In a comment to the last post, Urs raised what I think is one of the central questions of current research in homotopy type theory. I would phrase it as what do we still need to add to homotopy type theory to obtain a complete internal language for -topoi?
Before we start trying to answer that question, we have to clarify one minor point. Since type theory is elementary in the technical sense (“finitary first-order”), we shouldn’t expect it to distinguish Grothendieck -toposes from “elementary” ones. There is not yet an accepted notion of “elementary -topos”, but we can try to “elementarify” characterizations of Grothendieck -topoi. For instance, by the “-Giraud theorem”, Grothendieck -topoi are the locally presentable (∞,1)-categories in which colimits are stable under pullback, coproducts are disjoint, and internal groupoids are effective. The latter two conditions can also be replaced by the existence of classifiers for -compact objects for all sufficiently large .
A different jumping-off point is that since higher topoi naturally point us in a predicative direction, we can try to generalize the axioms people have come up with for “predicative versions of topoi.” For instance, we can try to -ize a Π-W-pretopos: a locally cartesian closed pretopos with W-types. It’s common in predicative mathematics to also assume some universes.
So what, of this, do we have already from homotopy type theory?
Intensional type theory with function extensionality corresponds (morally, anyway) to a locally cartesian closed -category. Of course this implies that whatever colimits exist are stable under pullback (although as we saw in the comments it can take a bit of work to prove that in the type theory). In the locally presentable case, the converse follows from the adjoint functor theorem: if colimits are stable under pullback, then the category is locally cartesian closed.
Adding the univalence axiom, as we discussed last time, corresponds to having object classifiers, which are the -categorical version of universes. Note, though, that instead of saying that the object classifiers classify “all -compact objects” as we usually do for Grothendieck -topoi (for some external cardinal ), we say that the objects they classify are closed under dependent sums and products. This is like having an inaccessible cardinal internal to the -category.
- A digression: Let me give you my three-sentence sketch of Voevodsky’s theorem that univalence (plus the “eta rule”) implies function extensionality. Ordinary dependent type theory, with “beta and eta rules”, gives a locally cartesian closed 1-category: we have (in the non-dependent case) functors and with transformations and , and the beta and eta rules are the two triangle identities. Function extensionality is about local cartesian closure of the -category of types, i.e. an -adjunction —but the -triangle identities are pointwise, so it suffices to ensure that the functors and natural transformations involved are -functors and -transformations, i.e. they respect homotopies. However, univalence ensures that all type-theoretic constructions are functorial on equivalences and homotopies between them; and by a path-object argument, that suffices to also make them functorial on homotopies between maps that aren’t equivalences.
Of course, W-types are already a type-theoretic notion which has been imported into set theory. In particular, the inductive types of Coq and Agda include W-types. (I think they are strictly more general; can any type-theorist in the audience tell me the 1-categorical structure which corresponds to extensional type theory with the inductive types of Coq/Agda?). Coq and Agda also have coinductive types, which should make David Corfield happy.
We concluded in the other thread that inductive types in type theory also include (finite) disjoint coproducts, even in the -categorical sense.
So all that’s missing from the properties we considered above for “elementary -topoi” is
(Some elementary shadow of) local presentability, and
Effectiveness of internal groupoids (i.e. “-exactness”).
Perhaps the most obvious elementary shadow of local presentability is the existence of finite colimits. We could try to add these axiomatically, but it would be more satisfying to derive them from some more type-theoretic structure, the way inductive types give us coproducts. So let’s come back to that in a bit; for now let’s think about effectiveness of internal groupoids.
An internal groupoid in an -category just means the ordinary notion of internal category together with inverses for morphisms, except that everything is “homotopified”. That is, we have an object-of-objects , an object-of-morphisms with source and target maps , a unit map and a composition map , which are unital and associative up to all higher homotopies. There are various ways of making the latter precise, depending somewhat on your model for -categories. For instance, Lurie uses internal simplicial objects which satisfy a homotopy version of the condition to be the nerve of a groupoid; see here.
Three examples of internal groupoids that you should keep in mind are:
If is a set (a 0-type), and is an equivalence relation on (in the 1-category of 0-types), then is an internal groupoid.
More generally, any internal groupoid, in the 1-categorical sense, in the 1-category of 0-types, is an internal groupoid.
If is an internal group object (in particular, if it is a 1-group, i.e. a group in the 1-category of 0-types), then is an internal groupoid.
Now what does it mean for a groupoid to be effective? Any morphism has a kernel or Cech nerve , which is an internal groupoid in a straightforward way. If is an internal groupoid with , we say that descent data under for a morphism is a morphism of groupoids that is the identity on . A quotient of is an initial object in the category of morphisms equipped with descent data. And finally, is effective if it has a quotient of which it is the kernel, i.e. so that the map is an equivalence.
To make sense of that, let’s see what it means in the above three examples.
For sets and , the kernel of a function is the equivalence relation on defined by if . Thus, has descent data for an equivalence relation iff implies . Hence a quotient of is a coequalizer of , and is effective if it is the kernel of its coequalizer. This is the usual notion of exactness for 1-categories.
If is a set, is a 1-groupoid, and is a map, then is an internal groupoid in sets for which . At least in the usual model where 1-groupoids are constructed in terms of sets, to give descent data under an internal groupoid in sets just means to give a functor from that groupoid to which agrees with on objects. Thus, an effective quotient of a groupoid is just that groupoid, regarded as an object of the category of groupoids rather than an internal groupoid in the category of sets.
Finally, for any type and any morphism , the kernel of is also called the loop object of based an , . Therefore, if is an internal group object, then an effective quotient of the internal groupoid is, in particular, a type with a morphism such that as group objects.
In other words, the classical homotopy-theoretic loop space recognition principle is a special case of effectiveness of internal groupoids. In particular, with effective internal groupoids we can construct “Eilenberg-Mac Lane” objects, and hopefully even “spectra.”
Effectiveness of internal groupoids should also be useful for constructing truncations. Suppose is any type, and consider the “codiscrete groupoid” . An effective quotient of this groupoid is a (-1)-truncation , a notion which we mentioned earlier that we might want to be able to construct. I believe we can go on and construct higher truncations in this way as well. For instance, an effective quotient of , where , should be a 0-truncation of , and so on.
Finally, we can also hope to construct colimits in this way. In the 1-categorical case, it’s a theorem that a --pretopos has finite colimits: the idea is that we can construct a coequalizer of as the quotient of the equivalence relation generated by and . We need the and (or at least an exponentiable natural-numbers-object) to construct this equivalence relation. We can hope to “homotopify” this idea to construct “freely generated groupoids” in type theory with inductive types, and thereby construct colimits as the quotients of such groupoids. So if we can resolve the second missing axiom, it may resolve the first one for us.
So what’s the problem with adding “internal groupoids are effective” as an axiom to homotopy type theory? Well, it’s not elementary, at least not a priori. The “all higher homotopies” condition in the definition of an internal groupoid involves an infinite amount of data. Now we do have ways to talk about infinite collections of data in type theory, using inductive and coinductive types: a good example is the natural numbers, which are infinite and also one of the simplest inductive types. So we can hope to use inductive and/or coinductive types to define a notion of “internal groupoid” inside the type theory, so that we could then state the axiom “internal groupoids are effective.” Several groups of people are working in such directions, and I think the prospects are good for eventual success.
Let me also remark in passing that a good definition of “internal groupoid” should of course really be a special case of a notion of “internal category”, and perhaps even of “internal -category”. In particular, we would need a notion of internal category (which, since it is internal to an -category, is automatically itself “”) in order to even state (let alone prove) something like “all finite diagrams have colimits,” although we could also rely on some externally known theorem like the constructibility of colimits from coproducts and pushouts.
On the other hand, the notion of “internal groupoid” we end up with may be fairly complicated, and it would be nice for the fundamental axioms to be simple and easily graspable, like (I think) univalence is. Thus we might hope to be able to derive exactness from something simpler.
Voevodsky has one idea for how to construct groupoid-quotients out of universes. Recall that the quotient of an equivalence relation on a set can be defined to be its set of equivalence classes, which is a subset of , where is the subobject classifier. The idea for the quotient of a groupoid , as I understand it, is to replace by , where is a (univalent) universe. Instead of a subset of this, we probably need to equip its points with extra structure corresponding to “descent data” under .
It seems to me that some additional axioms will be needed for this to work. The version for equivalence relations works because is the set of all truth values, but is not of course the type of all types. It seems plausible to me that with this idea we can construct an object that has the correct universal property of the quotient with respect to all types in , but I don’t see immediately how to extend that to types not in . Moreover, the quotient constructed in this way will not, itself, be an element of .
Motivated by similar considerations, Voevodsky has been experimenting with a general class of axioms he calls resizing axioms, which are all of the form “a type , guaranteed only to belong to a universe , can actually be considered as belonging to some smaller universe.” At Oberwolfach he mentioned explicitly three such axioms:
“A (-1)-type can be considered as belonging to any universe at all.” This seems more or less the same as the existence of a subobject classifier.
“If belongs to some universe and is equivalent to , then can also be considered as belonging to the same universe as .” This seems innocuous, but it also seems like it might be quite difficult to construct a set-theoretic model of.
“If is an element of some universe , then the full sub-type of consisting of all types equivalent to is again an element of .” The latter is of course a version of , so this axiom is more or less a particular case of exactness.
I don’t know whether these resizing axioms would guarantee that “quotients” constructed as above would lie in the same universe, or whether a different resizing axiom would be needed. If this construction does work, then there would undoubtedly be a certain elegance to it. But there are also other possible ways to construct quotients; my current plan is for the next post to discuss one such idea.
Re: Homotopy Type Theory, V
The second question Urs asked in his comment on the last post was
In principle, I think the answer is surely yes. There are definitely places in 1-topos theory where people have made use of an “internal language” that refers not only to a single topos, but to a pair of topoi related by a functor or an adjunction. The word “modal” often appears in this connection. For instance, a topos equipped with a Lawvere-Tierney topology (which can be regarded as two toposes related by a geometric embedding) has a corresponding “modal operator” which acts on its internal logic. The double-negation topology on the effective topos plays an important role. There is also the Awodey-Kishida sheaf semantics for modal logic, which David Corfield keeps bringing up in other posts. And there are surely other examples.
So what is the best way to describe the structure on a cohesive -topos induced by its “cohesiveness” over (or over some other -topos, for that matter)? We could assert a subcategory of “discrete objects” (via, for instance, a type constructor such that ) which is both reflective and coreflective and closed under finite products. But there might be some hidden gotcha there; I haven’t thought at all about how that would interact with dependent types. And then there are the codiscrete objects to add as well.